\documentclass[a4paper,12pt]{report}

\usepackage[francais]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{url}
\usepackage{amsmath}
\usepackage{multicol}

\title{Structures de données avancées 1}
\author{Université de Strasbourg}
\date{D'après le cours de Mme. Dominique Bechmann}

%\pagestyle{headings}

\begin{document}

\maketitle
\tableofcontents

\chapter{Rappels de programmation et introduction à la spécification}
\section{Programmation}
\subsection{Utilisations de types prédéfinis}
En C, il n'existe pas de type \url{bool}. On peut néanmoins en "créer" un.
\begin{verbatim}
typedef unsigned char bool
\end{verbatim}

On peut également définir le type \url{bool} de cette façon : tout ce qui est à 1 est vrai, le reste est faux :
\begin{verbatim}
# define faux 0
# define vrai 1
\end{verbatim}
Ou :
\begin{verbatim}
# define vrai (1=1)
# define faux (!vrai)
\end{verbatim}

Définissons quelques ensembles :
\begin{itemize}
\item[\textbullet][\textbullet]{Les entiers naturels, ou Nat : \begin{verbatim}typedef unsigned int Nat;\end{verbatim}}
\item[\textbullet][\textbullet]{Les entiers relatifs, ou Ent :\begin{verbatim}typedef int Ent;\end{verbatim}}
\item[\textbullet][\textbullet]{Les réels des langages de programmation sont en réalité des rationnels d'où :\begin{verbatim}typedef float Rat, Reel;\end{verbatim}}
\item[\textbullet][\textbullet]{Les caractères :\begin{verbatim}typedef char car;\end{verbatim}}
\end{itemize}

\subsection{Structures de données}
Pour des objets plus compliqués, il faut fabriquer soi-même un ou plusieurs types de données adaptées avec des tableaux, des structures ou des pointeurs.

\subsection{Programmation fonctionnelle}
Nous programmons sous forme de fonctions sans toucher aux paramètres.\\
\textbf{Exemple:} considérons des ensembles d'entiers naturels avec les opérations classiques sur les ensembles.

\begin{verbatim}typedef struct {Nat v[100]; Nat n;} Ens;\end{verbatim}

\'Ecrivons maintenant les opérations :

\begin{verbatim}
Ens ensVide ()   //ensemble vide
{
     Ens e;      //nouvel ensemble
     e.n=0;      //cardinal à 0
     return e;
}
\end{verbatim}
\`A cause du passage de paramètre par valeur (en C), la recopie de l'ensemble est automatique lors de l'appel de la fonction si il est en paramètre.

\begin{verbatim}
Ens insertion (Ens e, Nat x)   //insertion de x à la fin du tableau
{
     e.v[e.n]=x;
     e.n++;
}
\end{verbatim}

La recopie à chaque appel de fonction est un processus lourd mais obligatoire en programmation fonctionnelle.
\pagebreak
\'Ecrivons la fonction testant l'appartenance d'un élément à l'ensemble. La forme 1 de \url{app} est écrite en récursif :

\begin{verbatim}
Bool app(Ens e, Nat x)
{
     if(e.n == 0) return faux;
     else if(e.v[e.n-1] == x) return vrai;
     else
     {
           e.n --;
                  return app(e, x);
     }
}
\end{verbatim}

Il est désagréable de modifier \url{e} pour un simple parcours même si cela reste interne à la fonction \url{app}. On préférera la forme 2 de \url{app} appelant une fonction auxiliaire \url{app1}, avec un paramètre supplémentaire de position \url{k} sur lequel opère la récursivité.
\begin{verbatim}
Bool app1(Ens e, Nat x, Nat k)
{
     if(k==0) return faux;
     else if(e.v[k-1]==x) return vrai;
     else return app1(e, x, k-1);
}
        
Bool app(Ens e, Nat x)
{
     return app1(e, x, e.n);
}
\end{verbatim}

La forme 3, en remplaçant \url{app1} par une version itérative, évite les recopies d'ensemble. On recoupe tout dans \url{app}.
\begin{verbatim}
Bool app(Ens e, Nat x)
{
     Nat k;
     for(k=e.n; k>0 && e.v[k-1]!=x; k--);
     return k!=0;
}
\end{verbatim}

\subsubsection{Autres fonctions:}

Cardinal:
\begin{verbatim}
Nat card(Ens e)
{
     return e.n;
}
\end{verbatim}

Test de vacuité:
\begin{verbatim}
Bool vide(Ens e)
{
     return e.n==0;
}
\end{verbatim}

Suppression : le dernier élément de l'ensemble prend la place de celui supprimé.

Écrivons une opération de recherche de minimum sous forme itérative.
\begin{verbatim}
Nat min(Ens e)
{
     Nat m = e.v[e.n-1];
     Nat k;
     for(k=e.n-1; k>0; k--)
          {
          if(e.v[k-1]<m) m=e.v[k-1];
          }
     return m;
}
\end{verbatim}
\subsection{Rappels sur les pointeurs}
\subsubsection{Simulation d'un passage par adresse :} 
On remplace la transmission d'un paramètre (structure) par son adresse \url{&x} qui est recopiée lors de l'appel de la fonction. 
L'objet \url{x} peut être modifié, il est muté. On parle de programmation avec mutation.

\subsubsection{Allocation dynamique:}
En langage, C, la fonction \url{malloc} permet d'allouer une zone mémoire et de renvoyer un pointeur sur cette zone. Couplé avec
la fonction \url{sizeof} qui fournit le nombre d'octets nécessaire, on obtient l'allocation dynamique \url{malloc(sizeof(t));}, où \url{t}
est un type fourni en paramètre.\\

Pour simplifier l'écriture, on définit quelques macros :
\begin{verbatim}#define MALLOC(t) ((t*)malloc(sizeof(t)))
#define SIZEOF(t) ((Nat)sizeof(t))\end{verbatim}

Et pour allouer une zone \url{n} fois, nous définissons :
\begin{verbatim}#define MALLOCN(n,t) ((t*)malloc(n*sizeof(t)))\end{verbatim}

Et une version qui initialise à 0 tous les octets de la zone :
\begin{verbatim}#define CALLOC(n,t) ((t*)calloc(n,sizeof(t)))\end{verbatim}

Enfin, le pointeur vers aucune zone mémoire (pointeur nul) :
\begin{verbatim}#define NULL (void*)0\end{verbatim}

\subsection{Programmation avec mutations}
Reprenons la structure :
\begin{verbatim}
typedef struct StrEns {Nat v[100]; Nat n;} Ens;
\end{verbatim}

Nous allons utiliser la simulation du passage par adresse avec les pointeurs et donc modifier l'ensemble par "effet de bord".
\begin{itemize}
\item[\textbullet]{\url{forme1} sera écrite avec des procédures.}
\item[\textbullet]{\url{forme2}, nous laisserons aux opérations un aspect fonctionnel en écrivant des fonctions.}
\end{itemize}

Forme 1 :
\begin{verbatim}
void ensVide(Ens *e)
{
     e->n = 0;
}
        
void insert(Ens *e, Nat x)
{
     e->v[e->n]=x;
     (e->n)++;
}
        
void suppr(Ens *e, Nat x)
{
     Nat k;
     (e->n)--;
     for(k=(e->n); e->v[k]!=x; k--){e->v[k]=e->v[e->n];}
}
\end{verbatim}

Forme 2 :
\begin{verbatim}
Ens* ensVide( )
{
     Ens *e = MALLOC(Ens);
     e->n = 0;
     return e;
}
        
Ens* insert(Ens *e, Nat x)
{
     e->v[e->n]=x;
     e->n ++;
     return e;
}

Ens* suppr(Ens *e, Nat x)
{
     Nat x;
     (e->n)--;
     for(k=e->n; e->v[k]!=x; k--);
     e->v[k]=e->v[e->n];
     return e;
}
\end{verbatim}

\section{Spécifications}
\subsection{Un petit exemple}
Illustrons la démarche de résolution des problèmes que nous voulons mettre en place sur la définition de la fonction $x^n$, avec $x$ rationnel et $n$ entier.
Nous allons d'abord spécifier l'opération puis raffiner la spécification : 
\begin{enumerate}
\item{tout d'abord par rapport aux opérations de base,}
\item{ensuite de manière récursive "directe",}
\item{enfin de manière itérative pour préparer l'implantation en C.}
\end{enumerate}
\subsubsection{Spécification formelle :}
\textbf{Profil :}\begin{verbatim}puiss : Rat Nat -> Rat      //puissance\end{verbatim}
\textbf{Préconditions:}\begin{verbatim}n : Rat; x : Rat\end{verbatim}\begin{verbatim}puiss(x, n):x!=0 ou n!=0\end{verbatim}

\begin{enumerate}
\item{\begin{verbatim}puiss(x, 0)=1\end{verbatim}\begin{verbatim}puiss(x, n+1)=x*puiss(x, n)\end{verbatim} car $x^{(n+1)}=x*x^n$}
\item{\begin{verbatim}puiss(x, n)=1 si n==0, x*puiss(x, n-1) sinon\end{verbatim}}
\item{\begin{verbatim}puiss(x, n)=r avec (i, r)=init(n, 1) tq i!=0 rep(i-1, r*x)f.rep\end{verbatim}}
\end{enumerate}

\subsection{Spécification des ensembles}
On suppose connu un module de spécification de \url{BASE} avec des booléens, des entiers... avec leurs opérateurs habituels.

Spécification d'ensembles finis d'entiers naturels, tous distincts, dont le cardinal est borné par 100 :

Ensemble borné par N
\begin{verbatim}
typedef struct strens { Nat v[N]; Nat n; } StrEns, *Ens;              // Tableau statique
typedef struct strens { Nat *v  ; Nat n; Nat taille; } StrEns, *Ens;  // Tableau dynamique
\end{verbatim}

(e1) x $\in$ $\O$ = faux \\

(e2) x $\in$ i(x,y) = x==y $\vee$ x $\in$ e \\

(e3) v(\O) = vrai \\

(e4) v(i(e,x)) = faux \\ 

(e5) |\O| = 0 \\

(e6) |i(e,x)| = A + |e| \\

(e7) s(i(e,x),y) = si x==y alors e sinon i(s(e,y),x) fsi \\

(e8) m(i(e ,x)) = si |e|=0 alors x sinon si x<min(e) alors x sinon min(e) fsi fsi

\chapter{Piles, files et listes}

\section{Pile}

\subsection{Définition}

Les piles sont des conteneurs d'objets manipulés par les opérations fondamentales :
- Placé un objet sur la piles (Empiler)
- Accéder à l'objet au sommet de la pile
- Retirer l'objet en haut de la pile (Dépiler)

LIFO (Last In - First Out)

\subsection{Spécification}

\begin{verbatim}
spec :  PILE0 (TRIV) étend BASE
sorte : Pile // pile non bornées d'objets de sorte S
opérations :
        pilenouv: -> Pile         // générateurs //
        empiler: Pile S -> Pile   //   de base   //
        depiler: Pile -> Pile
        remplacer: Pile S -> Pile // remplacer le sommet
        sommet: Pile -> S
        vide: Pile -> Bool
        hauteur: Pile -> Nat
préconditions :
        pré depiler(P) = !vide(P)
        pré sommet(P)  = !vide(P)
        pré remplacer(P,x) = !vide(P)
axiomes p:pile ; x:s ; y:s : 
        vide(pilenouv()) = VRAI
        hauteur(pilenouv()) = 0
        depiler(empiler(p,x)) = p
        remplacer(empiler(p,x),y) = empiler(p,y)
        sommet(empiler(p,x)) = x
        vide(empiler(p,x)) = FAUX
        hauteur(empiler(p,x)) = hauteur(p)+1
\end{verbatim}

\subsection{Implantation contiguë et programmation fonctionnelle}

\begin{verbatim}
#define S int
#define Nat int
#define Bool char
#define VRAI 1
#define FAUX 0

typedef struct strpile{S v[N]; Nat h;} Pile; /* implantation avec piles bornés */

Pile pilenouv(){
  Pile p;
  p.h=0;
  return p;
}

// Préconditions : p.h<N
Pile empiler(Pile p, S x){
  p.v[p.h]=x;
  p.h++;
  return p;
}

// Préconditions : vide(p) = FAUX
Pile depiler(Pile p){
  p.h--;
}

// Préconditions : vide(p) = FAUX
Pile remplacer(Pile p, S x){
  return empiler(depiler(p),x);
}

// Préconditions : vide(p) = FAUX
S sommet(Pile p){
  return p.v[p.h-1];
}

Bool vide(Pile p){
  return p.h==0;
}

Nat hauteur(Pile p){
  return p.h;
}
\end{verbatim}

\subsection{Implantation contiguë et programmation avec mutation}

\begin{verbatim}
typedef struct strpile{S v[N]; Nat h;} Pile; /*forme 1*/
typedef struct strpile{S v[N]; Nat h;} Pile; /*forme 2*/
typedef struct strpile{S v[N]; Nat h;} Strpile, *Pile; /*forme 3*/
\end{verbatim}

\subsubsection{Forme 1, procédurale:}

\begin{verbatim}
void pilenouv(){
  Pile* p;
  p->h=0;
}

// Préconditions : p.h<N
void empiler(Pile* p, S x){
  p->v[p->h]=x;
  p->h++;
}

// Préconditions : vide(p) = FAUX
void depiler(Pile* p){
  p->h--;
}
\end{verbatim}
\pagebreak 
\begin{verbatim}
// Préconditions : vide(p) = FAUX
void remplacer(Pile* p, S x){
  p->v[p->h-1];
}

// Préconditions : vide(p) = FAUX
S sommet(Pile* p){
  return p->v[p->h-1];
}

Bool vide(Pile* p){
  return p->h==0;
}

Nat hauteur(Pile* p){
  return p->h;
}
\end{verbatim}

\subsubsection{Forme 2, fonctionnelle:}

\begin{verbatim}
Pile* pilenouv(){
  Pile* p=MALLOC(Pile);
  p->h=0;
  return p;
}

// Préconditions : p->h<N
Pile* empiler(Pile* p, S x){
  p->v[p->h]=x;
  p->h++;
  return p;
}

// Préconditions : vide(p) = FAUX
Pile* depiler(Pile* p){
  p->h--;
  return p;
}
\end{verbatim}
\pagebreak
\begin{verbatim}
// Préconditions : vide(p) = FAUX
Pile* remplacer(Pile* p, S x){
  empiler(depiler(p),x);
  return *p;
}

// Préconditions : vide(p) = FAUX
S sommet(Pile* p){
  return p->v[p->h-1];
}

Bool vide(Pile* p){
  return p->h==0;
}

Nat hauteur(Pile* p){
  return p->h;
}
\end{verbatim}

\subsubsection{Forme 3, pointeurs:}

\begin{verbatim}
Pile pilenouv(){
  Pile p=MALLOC(StrFile);
  p->h=0;
  return p;
}

// Préconditions : p->h<N
Pile empiler(Pile p, S x){
  p->v[p->h]=x;
  p->h++;
  return p;
}

// Préconditions : vide(p) = FAUX
Pile depiler(Pile p){
  p->h--;
}
\end{verbatim}
\pagebreak
\begin{verbatim}
// Préconditions : vide(p) = FAUX
Pile remplacer(Pile p, S x){
  return empiler(depiler(p),x);
}

// Préconditions : vide(p) = FAUX
S sommet(Pile p){
  return p->v[p->h-1];
}

Bool vide(Pile p){
  return p->h==0;
}

Nat hauteur(Pile p){
  return p->h;
}
\end{verbatim}

\subsection{Implantation par chaînage:}
On travaille sur des piles non bornées.
\begin{verbatim}
typedef struct StrPile {S v; struct StrPile* s;} StrPile, *Pile;
\end{verbatim}

On peut donc définir les opérations suivantes :

\begin{verbatim}
Pile PileNouv(){
  Pile p=NULL;
  return p;
}

Pile empiler(Pile p, S x){
  Pile new_p=MALLOC(StrPile);
  new_p->v=x;
  new_p->s=p;
  return new_p;
}

S Sommet(Pile p){
  return(p->v);
}

Bool vide(Pile p){
  return(p==NULL);
}

Pile depiler(Pile p){
  Pile p_buff=p;
  p=p_buff->s;
  free(p_buff);
  return p;
}

Pile remplacer(Pile p,S x){
  p=empiler(depiler(p),x);
  return p;
}

S hauteur(Pile p){
  S h=0;
  Pile p_buff=p;
  while(!vide(p_buff)){
    h++;
    p_buff=p_buff->s;
  }
  return h;
}
\end{verbatim}

Pour la suite, le deuxième bloc contiendra la hauteur de la liste :

\begin{verbatim}
Pile PileNouv(){
  Pile p=MALLOC(Pile);
  p->v=0;
  p->s=NULL;
  return p;
}

S sommet(Pile p){
  return(p->s->v);
}

Bool vide(Pile p){
  return(p->v==NULL);
}

Pile empiler(Pile p, S x){
  Pile new_p=MALLOC(StrPile);
  new_p->v=x;
  new_p->s=p->s;
  p->s=new_p;
  p->v++;
  return new_p;
}

Pile depiler(Pile p){
  p->s=p->s->s;
  p->v--;
  return p;
}

Pile remplacer(Pile p, S x){
  return p->s->v=x;
}
\end{verbatim}

\section{File}

Une file fonctionne sur le principe First In - First Out (FIFO).
On ajoute les éléments à la fin, en queue de file, et on accède aux éléments en tête de file.

Les opérations fondamentales sont :
\begin{itemize}
  \item{ajouter un élément en queue de file}
  \item{supprimer l'élément en tête de files}
  \item{accéder à l'élément en tête de file}
\end{itemize}

\subsection{Spécification}

Générateur de base :
\begin{itemize}
  \item{file vide}
  \item{ajouter un élément en queue}
\end{itemize}
Il permet de fabriquer toutes les files.\\

Spécifions des files génériques non bornés, d'objet de sorte $S$ apparaissant dans une spécification TRIV.\\

\begin{verbatim}
spec FILE0 (TRIV) étend BASE
sorte File // files non bornés
opérations :
  filenouv : -> file    // file vide
  adjq : file S -> file // ajout en queue
  supt : file S -> file // suppression en tête
  tete : file S -> S    // élément en tête
  vide : file S -> Bool // test de vacuité
  lgr  : file S -> Nat  // nombre d'éléments (optionnel)
\end{verbatim}

préconditions : f:file

tete(f) = $\neg$ vide(f)\\

axiomes : f:file ; x,y:S

(e1) vide(filenouv) = vrai

(e2) vide(adjq(f,x)) = faux

(e3) tete(adjq(f,x)) = si vide(f) alors x sinon tete(f) fsi

(e4) lgr(filenouv) = 0

(e5) lgr(adjq(f,x)) = 1+ lgr(f)

(e6) supt(filenouv) = filenouv

(e7) supt(adjq(f,x)) = si vide(f) alors filenouv sinon adjq(supt(f,x))

\subsection{Représentation contigüe}

Une file peut être representée par un tableau v de n élements, 

alloué statiquement S v[N];

alloué dynamiquement S* v; $\rightarrow$ ce qui convient pour des files non bornées

Il convient de noter le début et la longueur (ou le début et la fin)

La structure sera donc composé d'une tableau v , de la tête t, et de la longueur l \\

\begin{verbatim}
q = (t+l-1) % N
typedef struct {S v[N]; Nat t; Nat l; } File;
\end{verbatim}

\subsection{Représentation par chaînage}

On mémorise la tête et la queue de la file pour faire efficacement \url{adjq} et \url{supt}.

Déclaration en C de cette structure de données :\\

\begin{verbatim}
typedef struct strfile { S v; struct strfile* suiv; } Strfile;
typedef struct { Strfile* t; Strfile* q; } File;
\end{verbatim}

une file vide est donc une file \url{File} avec ses pointeurs \url{t} et \url{q} pointant sur \url{NULL}.

\begin{verbatim}
File filenouv(){
  File f;
  f.t = NULL; // Une file vide n'a ni tête
  f.q = NULL; // ni queue
  return f;
}

File adjq (File f, S x){
  Strfile* f1 = MALLOC(Strfile);
  f1->v = x;
  f1->suiv = NULL;
  if(f.t == NULL){
    f.t = f1;
    f.q = f1;
  }else{
    f.q->suiv = f1;
    f.q = f1;
  }
  return f;
}

File supt (File f){
  Strfile* buffer = f.t;
  if (f.t == f.q){
    if (f.t != NULL){
      f.t = NULL;
      f.q = NULL;
    }
  }else{
    f.t = f.t->suiv;
    FREE(temp);
  }
  return f;
}
\end{verbatim}

Une variante consiste à rendre la file circulaire et ainsi, nous n'avons plus besoin de connaître l'adresse de la tête.

\begin{verbatim}
typedef struct strfile {S v; struct strfile* suiv;} Strfile, *File;
\end{verbatim}

On peut donc re-définir toutes les opérations précédentes :

\section{Listes linéaires}
Une liste linéaire sur un ensemble $E$ est une suite finie $x_1, x_2, \dots, x_k$ d'éléments de $E$. On peut les noter $(x_1, x_2, \dots, x_k)$.
\subsection{Spécification de listes génériques non bornées}
\begin{verbatim}
spec LISTEO (TRIV) étend BASE
sorte Liste
\end{verbatim}
\subsubsection{Opérations:}
\begin{verbatim}
   listenouv : -> Liste
   adjt : Liste S -> Liste

   supt : Liste -> Liste
   tete : Liste -> S
   vide : Liste -> Bool
   longueur : Liste -> Nat
   app : Liste S -> Bool

   adjq : Liste S -> Liste
   supq : Liste -> Liste
   queue : Liste -> S
\end{verbatim}
\subsubsection{Préconditions:}
\begin{verbatim}
   pre(tete)=pre(queue)=non(vide(l))
\end{verbatim}
\subsubsection{Axiomes:}
\begin{verbatim}
Liste l; S x,y :
   (e1)supt(adjt(l,x))=l
   (e2)tete(adjt(l,x))=x
   (e3)vide(filenouv)=vrai
   (e4)vide(adjt(l,x))=faux
   (e5)longueur(listenouv)=0
   (e6)longueur(adjt(l,x))=1+longueur(l)
   (e7)app(filenouv,x)=faux
   (e8)app(adjt(l,x),y)=si (x=y) alors vrai sinon app(l,y)
   (e9)adjq(listenouv,x)=(x)
   (e10)adjq(filenouv,x)=adjt(filenouv,x)
   (e11)adjq(adjt(l,x),y)=si (vide(l)) alors adjt(adjt(listenouv,y)x) 
                          sinon adjt(adjq(l,y),x)
   (e12)supq(listenouv)=listenouv
   (e13)supq(adjt(l,x))=si (vide(l)) alors l sinon adjt(supq(l),x)
   (e14)queue(adjt(l,x))=si (vide(l)) alors x sinon queue(l)
\end{verbatim}
\subsubsection{Opérations sur le $i^{eme}$ élément:}
\begin{verbatim}
_[_] : Liste Nat -> S              /*l[i] ou elem(l,i)*/
ins : Liste Nat S -> Liste         /*insertion en ieme position*/
sup : Liste Nat -> Liste           /*suppression du ieme élément*/
chag : Liste Nat S -> Liste        /*remplacement du ieme élément*/
\end{verbatim}
\subsubsection{Précondition:}
\begin{verbatim}
pre l[i] = 1<=i<=lgr(l) et non(vide(l))
pre ins(l,i,x) = 1<=i<=lgr(l)+1

\end{verbatim}
\subsubsection{Axiomes:}
\begin{verbatim}
elem(adjt(l,x)i)=si (i=1) alors x sinon elem(l,i-1)
ins(listenouv,i,x)=adjt(listenouv,x)
ins(adjt(l,x),i,y)=si (i=1) alors adjt(adjt(l,x),y) 
                   sinon adjt(ins(l,i+1,y),x)
sup(adjt(l,x),i)=si (vide(l)) alors listenouv 
                 sinon adjt(sup(l,i-1),x)
chg(adjt(l,x),i,y)=si (vide(l) || (i=1)) alors adjt(l,y) 
                   sinon adjt(chg(l,i-1,y),x)
lig(listenouv,i)=listenouv;
lig(adjt(l,x),i)= si i<=1 alors listenouv sinon
                  si i>lgr(l)+1 alors l sinon
                  adjt(lig(l,i-1))
lid(listenouv,i)=listenouv;
lid(adjt(l,x),i)= si i<1 alors adjt(l,x) sinon
                  si i>lgr(l) alors listenouv
                  sinon lid(l,i-1)
sup1(listenouv,i)=listenouv;
sup1(adjt(l,x),i)=si x==i alors l sinon
                  adjt(sup1(l,i),x);
chg1(listenouv,i)=listenouv;
chg1(adjt(l,x),i,y)=si x==i alors adjt(l,y) sinon
                  adjt(chg1(l,i,y));
conc(listenouv,l)=l;
conc(l,listenouv)=l;
conc(adjt(l1,x),l2)=adjt(conc(l1,l2),x);
conc(l1,adjt(l2,x))=conc(adjq(l1,x),l2);

\end{verbatim}
Quelques variantes : \\
Il est possible de spécifier les opérations ``hors noyau'' non pas par rapport aux générateurs de base, mais ``directement''
\begin{verbatim}
ex : adjq(l,x) = si vide(l) alors adjt(listenouv,x) 
                 sinon adjt(adjq(supt(l),x),tete(l))
     supq(l) = si lgr(l)==1 alors listenouv 
                 sinon adjt(supq(supt(l)),tete(l))
\end{verbatim}
Attention : Une telle programmation conduit à des exécutions inefficaces.
\\
Pour préparer la programmation, nous allons raffiner la spécification en y introduisant des préoccupations d'efficacité
( ex = parcours sur les listes à minimiser)
\\
Ex : sur l'opération donnant le ieme element :
pré l[i]=1<=i<=lgr(l)
\\
1. Spécification par rapport aux générateurs de base\\
    adjt(l,x)[i] = si i==1 alors x sinon l[i-1]
\\
2. Spécification directe\\
    \begin{verbatim}l[i] = si i==1 alors tete(l) sinon supt(l)[i-1]\end{verbatim}
        ou bien
    \begin{verbatim}l[i] = si i==lgr(l) alors queue(l) sinon supq(l)[i]\end{verbatim}

Dans ces deux versions, il apparait un sens de parcours des listes, de gauche
à droite pour la première et de droite à gauche pour la seconde
\\
3. Spécification itérative\\
    \begin{verbatim}(l1,k) = init(l,1) tantque (k<i) rep (supt(l1),k+1) frep\end{verbatim}

\subsection{Implantation des listes par contiguïté}

Une liste occupe un ensemble de places contiguës représentées 
par un tableau et comme elle peut commencer et finir n'importe ou dans le tableau,
on a intérêt à noter la longueur et l'indice de tête (comme pour les files).

\begin{verbatim}
typedef struct { S tab[N] ; Nat h ; Nat l; }

+ opérations efficaces : tête, queue de liste
- opérations au "milieu" peu efficaces (insertion, suppression)


\end{verbatim}

\subsection{Implantation par chaînage}

De manière analogue aux piles et aux files, on peut chaîner les éléments.

\begin{verbatim}
typedef struct strliste { S v ; struct strliste *s ;} Strliste, *Liste;

+ opérations en tête
+ insertion
+ permutations
- opérations en queue
- changements
\end{verbatim}

On peut également utiliser une liste chainée circulaire (le dernier élément pointe sur la tête),
ou une liste doublement chainée (bilatère / symétrique / bidirectionnelle ).
\\
Exemple de liste doublement chainée :
\begin{verbatim}
typedef struct strliste{struct strliste *p ; S v ;
                        struct strliste *s ;} Strliste, *Liste;
\end{verbatim}

\begin{verbatim}
liste chainée simple :
  - l[i] ?
  - les op. du noyau

typedef struct strliste{ S v; struct strliste *s;} Strliste, *Liste;

Liste filenouv(){
    Liste l;
    l->s = NULL;
}

Liste adjt(Liste l, S x){
    Liste buff;
    buff=malloc(sizeof(Strliste));
    if(l==NULL){
        l=buff;
        l->s=l;
        l->v=x;
    }else{
        buff->s = l;
        buff->v = x;
        l=buff;
    }
}

/* pré : 1<=i<=lgr(l) */
S ieme(Liste l, S i){
    if(i==1) return l->v;
    else return ieme(l->s,i-1);
}

/* pré : liste non vide */
Liste supt(Liste l){
    Liste buff = l;
    l=l->s;
    free(l);
}

Bool vide(Liste l){
    return l==NULL;
}

Liste app(Liste l, S x){
    Bool trouve = false;
    while(l!=NULL && trouve==false){
        if(l->v==x) trouve=true;
        l=l->s;
    }
    return trouve;
}

S queue(Liste l){
    while(l->suiv!=NULL){
        l=l->s;
    }
    return l->v;
}

Liste changerieme(Liste l, S x, Nat i){
   if(i==1){
        l->v=x;
        return l;}
    else changerieme(l->s,x,(i-1));
}

/* pré : !vide(l) && 1<=i<=lgr(l) */
Liste supprieme(Liste l, Nat i){
    if(i==1) supt(l);
    else supprieme(l->s,(i-1));
}

Liste insieme(Liste l, S x, Nat i){
    if(i==1){
        adjt(l,x);
        return(l);
    }
    else insieme(l->s,x,(i-1));
}
\end{verbatim}
\pagebreak
\begin{verbatim}
S lgr(Liste l){
    Liste buff=l;
    S n=0;
    while(buff!=NULL){
        buff=buff->s;
        n++;
    }
}

S dernier(Liste l){
    return ieme(l,lgr(l));
}

S avantdernier(Liste l){
    return ieme(l,(lgr(l)-1));
}

/* pré : non(vide(l)) */
Liste adjq(Liste l, S x){
    Liste tmp=MALLOC(Liste);
    tmp->s=NULL;
    tmp->v=x;
    dernier(l)->s=tmp;
    return l;    
}

/*pré : non(vide(l)) */
Liste supq(Liste l){
    Liste tmp;
    if(!vide(l))
        if(l->s==NULL){free(l);l=NULL;}
        else{
            tmp=avantdernier(l);
        free(tmp->s);
        tmp->s=NULL;
        }
    return l;
}
\end{verbatim}
\pagebreak
\begin{verbatim}
Liste lig(Liste l){
    Liste lig;
    Nat milieu=adresseieme(l,lgr(l)/2);
    S i;
    for(i=0;i<milieu;i++){
        adjq(lig,l[i]);
    }
    return lig;
}

liste lid(Liste l){
    Liste lid;
    Nat milieu=adresseieme(l,lgr(l)/2);
    S i;
    for(i=milieu;i<lgr(l);i++){
        adjq(lid,l[i]);
    }
    return lid;
}
\end{verbatim}

\section{Une hiérarchie de sortes avec un ordre sur les éléments}
Sorte S définie par une théorie dite triviale :
\begin{verbatim}
spec TRIV etend BOOL
sorte S
fspec
\end{verbatim}

Si une relation binaire d'égalité notée \url{==} est nécessaire, alors la sorte S est définie par la théorie suivante :
\begin{verbatim}
spec EG etend TRIV
operations
    ==, != : S S -> Bool /* Egalité, différence */
axiomes
    (e1) x==x = vrai /* réfléxivité */
    (e2) x!=y = non(x==y)
fspec
\end{verbatim}

\subsection{Rappels mathématiques}
\subsubsection{Définitions:}
Un préordre sur un ensemble $E$ est une relation binaire dans $E$ notée habituellement $\geq$. Cette relation est réfléxive et 
transitive.

La relation notée $\sim$ définie par $x \sim y = x\geq y$ et $y\geq x$ est une relation d'équivalence.

Un ordre est un préordre antisymétrique, \textit{i.e.} $((x\geq y$ et $y\geq x)\Rightarrow x==y)=vrai$.

Une relation binaire $\geq$ sur $E$ est dite totale si pour tout couple $(x,y)$ de $E\times E$ alors $x\geq y$ ou $y\geq x$. Dans ce cas, $==$ et $=\sim$ coïncident.

\subsubsection{Exemple:}
Prenons pour exemple le type \url{Personne}, déclaré en C : 
\begin{verbatim}
typedef struct {Chaine nom; Nat num;}Personne;
\end{verbatim}

Nous pouvons y définir une relation de préordre $\geq$ ainsi : pour tout couple $(x,y)$ de personnes, $x\geq_E y$ ssi $x.nom \geq_{ch} y.nom$. Vérifions que cette relation est un préordre mais pas un ordre.

\section{Listes triées}
\subsection{Spécification}

\subsection{Recherche dans une liste triée}
\subsubsection{Spécification par rapport aux générateurs}

\subsubsection{Spécification de recherche séquentielle}

\subsubsection{Spécification de recherche dichotomique}
\begin{verbatim}
rech(l,x)=rdich(l,x,1,lgr(l))
avec rdich(l,x,a,b)=si b>a alors 0
     sinon si l[m]==x alors m
     sinon si l[m]<x alors rdich (l,x,m+1,b)
     sinon rdich(l,x,a,m-1) fsi fsi
     avec m=E((a+b)/2)
\end{verbatim}
A dérouler sur un exemple.

\section{Listes circulaires}
\begin{verbatim}
spec LISTECIRC etend BASE
sort Listec
\end{verbatim}
\subsubsection{Opérations:}
\begin{verbatim}
   listenouv : -> Listec
   adjt, adjq : Listec S -> Listec
   supt,supq : Listec -> Listec
   ev : Listec -> Bool
   suiv : Listec -> Listec
   ieme : Listec -> S
   long : Listec -> Nat
   t : Listec -> S
   q : Listec -> S
\end{verbatim}
\subsubsection{Préconditions:}
\begin{verbatim}
   pre(supt)=pre(supq)=non(ev(l))
   pre(ieme)=non(ev(l))
   pre(t)=pre(q)=non(ev(l))
\end{verbatim}
\subsubsection{Axiomes:}
\begin{verbatim}
Listec l; S x,y :
   (e1)adjq(filenouv,x)=adjt(filenouv,x)
   (e2)adjq(adjt(l,x),y)=si (vide(l)) alors adjt(adjt(listenouv,y)x) 
                          sinon adjt(adjq(l,y),x)
   (e3)supt(adjt(l,x))=l
   (e4)supq(listenouv)=listenouv
   (e5)supq(adjt(l,x))=si ev(l) alors l sinon adjt(supq(l),x)
   (e6)ev(listenouv)=vrai
   (e7)ev(adjt(l,x))=faux
   (e8)suiv(listenouv)=listenouv
   (e9)suiv(adjt(l,x))=si ev(l) alors adjt(l,x) sinon adjq(l,x)
   (e10)ieme(adjt(l,x),i)=si (i==1) alors x sinon ieme(l,(i-1))
   (e11)long(listenouv)=0
   (e12)long(adjt(l,x))=si ev(l) alors 1 sinon 1+long(l)
   (e13)t(adjt(l,x))=x
   (e14)q(adjt(l,x))=si ev(l) alors x sinon q(l)
\end{verbatim}

On choisit une structure de données adaptée : 
\begin{verbatim}
typedef struct strliste{S v; struct strliste *s} Strliste, *Liste;
\end{verbatim}

On peut donc programmer les fonctions :
\begin{verbatim}
Listec Listecnouv(){
    Listec l = NULL;
    return l;
}

Listec AdjTete(Listec l, S x){
    Listec tete = malloc(sizeof(Strlistec));
    Listec buff = l;
    tete.v = x;
    tete.s = l;
    while(buff->s != l) buff = buff->s;
    buff->s=tete;
    l=tete;
    return l;
}

Listec AdjQueue(Listec l, S x){
    AdjTete(l,x);
    l=l->suiv;
    return l;
}

Listec Suptete(Listec l){
    Listec buff=NULL,buff2=NULL;
    while (buff->s != l) buff=buff->s;
    buff2 = l;
    buff->s = l->s;
    free(buff2);
}
\end{verbatim}
\pagebreak
\begin{verbatim}
Listec SupQueue(Listec l){
    Listec buff=NULL,buff2=NULL;
    while ((buff->s)->s != l) buff=buff->s;
    buff2=buff->s;
    buff->s = l;
    free(buff2);
}

Bool EstVide(Listec l){
    return l==NULL;
}

Listec suiv(Listec l){
    l=l->s;
    return l;
}

S ieme(Listec l, int i){
    Listec buff=l;
    for(;i>1;i++){
        buff=buff->s;
    }
    return buff->v;
}

int long(Listec l){
    Listec buff=l;
    int i=0;
    while(buff->s != l){
        buff=buff->s;
        i++;
    }
    return i;
}
\end{verbatim}

\pagebreak

Spécifier l'opérateur \url{flavius} et les opérateurs auxiliaires pour résoudre le problème suivant :
\begin{quotation}
En 67 avant J.C., 40 ennemis furent faits prisonniers. Ne voulant pas devenir esclaves, ils décidèrent de se mettre en cercle (liste circulaire) et de se numéroter périodiquement de 1 à 7. Chaque 7$^{eme}$ fut alors tué (supprimé de la liste) jusqu'à ce qu'il n'en reste plus qu'un, ce dernier devant se suicider. Le futur historien Flavius se plaça de façon à être le dernier... et ne se suicida pas. Déterminer la place choisie par Flavius dans le cercle.
\end{quotation}

\subsubsection{Décomposition fonctionnelle :}
\begin{verbatim}
init : -> Listec                   /* Construction d'une liste 
       Listec Nat -> Listec        circulaire de 40 personnes
                                   numérotées de 1 à 40 */

rotation : Listec Nat -> Listec    /* 6 permutations à gauche */
           Listec -> Listec

calcul : Listec Nat -> Listec      /* Suppression de 39 personnes */

flavius : -> Nat                   /* Numéro de la dernière personne */
\end{verbatim}

\subsubsection{Spécification, en mode récursif :}
\begin{verbatim}
init(l)=initaux(v(),i) avec initaux(l,i)=si (i==41) alors l
        sinon initaux(adjq(l,i),i+1); fsi

rotation(l)=l1 avec init(l,1) tant que (i<7) rep suiv(l1),i+1

calcul(l)=si (i==40) alors l sinon calcul(supt(rotat(l,1)),i+1) fsi

flavius()=tete(calcul(l,1)) avec l=init();
\end{verbatim}

\subsubsection{Implantation en C, en mode récursif :}
\begin{verbatim}
Listec init(Listec l, Nat x){
   
}

Listec rotation(Listec l){
   
\end{verbatim}

\subsubsection{Spécification, en mode itératif :}
\begin{verbatim}
init(l)=l avec (l,i)=init(v(),i) tant que (i<41) faire (adjq(l,i),i+1)

rotation(l)=si (i==7) alors l sinon rotation(suiv(l),i+1) fsi

calcul(l)=l1 avec (l1,i)=init(l,1) tant que (i<40) rep (supt(rotation(l1)),i+1)

flavius()=tete(calcul(l,1)) avec l=init();
\end{verbatim}

\subsubsection{Implantation en C, en mode itératif :}
\begin{verbatim}
Listec init(){
   Listec l=listnouv();
   for(i=1;i<41;i++) adjq(l,i);
   return l;
}
\end{verbatim}

\section{Listes pointées}

On définit un nouveau type de liste : les listes pointées, qui étend le type liste.
\subsubsection{Opérations:}
\begin{verbatim}
comp : Liste Liste -> ListePointee
debut, fin : ListePointee -> Liste
fenetre : ListePointee -> S
ap : ListePointee S -> ListePointee
               /* ajoute un élément à droite de la coupure */
sp : ListePointee -> ListePointee
               /* suppression de l'élément dans la fenêtre */
init, term : ListePointee -> ListePointee
               /* placement de la coupur een début ou fin de liste */
dqsg, dcpd : ListePointee -> ListePointee
               /* décalage de la coupure à gauche ou à droite */
\end{verbatim}

\subsubsection{Implantation:}
On utilisera deux listes chaînées circulaires avec pointeur sur la queue.

%Listec init(){
%   Listec l = 40*MALLOC(Listec);
%   l->s=NULL;
%   Nat i;
%   for(i=0;i<40;i++){
%      l[i].v=i+1;
%      l[i]->s=l[(i+1)%40]
%   }
%   return l;
%}
\end{document}